ds:Top, da:k:Knd fp Type, x, T:Top, ks:Knd List, tr:Top, j, i:Id.
R-da(R-state-var(i;ds;da;x;T;ks;tr);j)
=
if i = j reduce(k,d1. k : Valtype(da;k)  d1;;ks) else  fi
 k:Knd fp Type 

latex

Definitions

reduce(f;k;as), <a,b>, s = t, KindDeq, x. t(x), x:A. B(x), x.A(x), f  g, x:AB(x), P  Q, P  Q, x:AB(x), P & Q, P  Q, Valtype(da;k), x : v, Id, Prop, b, A, b, , a = b, Unit, left+right, es realizer ind Reffect compseq tag def, R-da(R;i), if b t else f fi, Top, IdDeq, f(a), @loc effect knd(v:T)  x := f State(ds) v , Void, x:A. B(x), type List, S  T, es realizer ind Rframe compseq tag def, es realizer ind Rplus compseq tag def, R-state-var(i;ds;da;x;T;ks;tr), , Type, Knd, a:A fp B(a), t  T, s ~ t, {T}, SQType(T)

Lemmas

R-da-Rall, top wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, Id wf, fpf-single wf, ma-valtype wf, fpf-empty wf, fpf-empty-join, reduce wf, fpf-join wf, fpf wf, Knd wf, Kind-deq wf